package mac5789.phase;

import java.util.ArrayList;
import java.util.List;
import java.util.Random;
import java.util.concurrent.Callable;
import java.util.concurrent.ExecutorService;
import java.util.concurrent.Future;

import mac5789.sat.RandomSatProblem;
import mac5789.solver.SatSolver;

/**
 * Medidor de satisfatibilidade que executa um número fixo de vezes de experimentos.
 * @author lundberg
 *
 */
public class FixedRunsSatisfiabilityMeasurer implements SatisfiabilityMeasurer {
	
	private ExecutorService executor;
	
	private final int runs;
	
	private final Random random;
	
	private final SatSolver solver;
	
	/**
	 * Construtor
	 * @param solver solver
	 * @param seed seed
	 * @param runs runs
	 */
	public FixedRunsSatisfiabilityMeasurer(SatSolver solver, ExecutorService executor, long seed, int runs) {
		super();
		this.solver = solver;
		this.random = new Random(seed);
		this.runs = runs;
		this.executor = executor;
	}

	/**
	 * {@inheritDoc}
	 */
	@Override
	public double measure(final int nVariables, final int nClauses) {
		int satisfiables = 0;
		List<Future<Boolean>> results = new ArrayList<Future<Boolean>>(runs);
		for(int i = 0; i < runs; i++) {
			results.add(executor.submit(new Callable<Boolean>() {
				@Override
				public Boolean call() throws Exception {
					return solver.solve(aRandomProblemWith(nVariables, nClauses)).isSatisfiable();
				}
			}));
		}
		for(Future<Boolean> result : results) {
			try {
				if(result.get()) {
					satisfiables++;
				}
			} catch (Exception e) {
				executor.shutdownNow();
				throw new RuntimeException(e);
			}
		}
		return (1.0 * satisfiables) / runs;
	}

	/**
	 * Cria um novo problema aleatório com o número dado de variáveis e cláusulas.
	 * @param nVariables nVariables
	 * @param nClauses nClauses
	 * @return RandomProblem
	 */
	private RandomSatProblem aRandomProblemWith(int nVariables, int nClauses) {
		return new RandomSatProblem(random.nextLong(), nVariables, nClauses);
	}
}
